the_es:event_system{i:l}, e',e:es-E(the_es). decidable(es-locl(the_es; e; e')) 

latex

Definitions	x:A. B(x), t  T, prop{i:l}, P  Q, x. t(x), decidable(P), P  Q, guard(T), P  Q, wellfounded{i:l}(A; x,y.R(x;y)), x(s), P  Q, P  Q
Lemmas	es-locl-wellfnd, es-E wf, decidable wf, es-locl wf, decidable assert, es-first wf, event system wf, es-first-implies, decidable functionality, not wf, assert wf, es-pred wf, es-locl-iff, decidable and, decidable not, decidable or, decidable es-E-equal, es-pred-locl